(* -*-sml-*- *)
(*****************************************************************************)
(* Sanity checking "ExecuteSemantics": a derived executable semantics        *)
(* Not for compiling.                                                        *)
(*****************************************************************************)

loadPath := "../official-semantics" :: "../regexp" :: !loadPath;
app 
 load 
 ["bossLib","metisLib","intLib","stringLib","pred_setLib",
  "regexpLib","ExecuteSemanticsTheory","PropertiesTheory"];

quietdec := true;
open bossLib metisLib intLib stringLib rich_listTheory
open regexpLib FinitePSLPathTheory UnclockedSemanticsTheory ExecuteSemanticsTheory;
quietdec := false;

(******************************************************************************
* Set default parsing to natural numbers rather than integers 
******************************************************************************)
val _ = intLib.deprecate_int();

(******************************************************************************
* Version of Define that doesn't add to the EVAL compset
******************************************************************************)
val pureDefine = with_flag (computeLib.auto_import_definitions, false) Define;

(******************************************************************************
* Evaluating expressions of the form x IN {y1; y2; ...; yn}
******************************************************************************)

(* For the current set of Sugar2 example properties, the following INSERT
   theorems seem to work better than this general conversion.
val _ = 
 computeLib.add_convs
  [(``$IN``,
    2,
    (pred_setLib.SET_SPEC_CONV ORELSEC pred_setLib.IN_CONV EVAL))];
*)

val () = computeLib.add_funs
  [pred_setTheory.IN_INSERT,
   pred_setTheory.NOT_IN_EMPTY];

(******************************************************************************
* Evaluating Sugar2 formulas
******************************************************************************)
val _ = computeLib.add_funs
         ([PSLPathTheory.SEL_REC_AUX,
           UF_SEM_F_UNTIL_REC,
           B_SEM,
           EVAL_US_SEM,
           EVAL_UF_SEM_F_SUFFIX_IMP,
           UF_SEM_F_STRONG_IMP_F_SUFFIX_IMP]);

(******************************************************************************
* For simplification during symbolic evaluation of Sugar2 formulas
******************************************************************************)

val EXISTS_COND = prove
  (``!p c a b.
       EXISTS p (if c then a else b) = if c then EXISTS p a else EXISTS p b``,
   RW_TAC std_ss []);

val COND_SIMP = prove
  (``!c a b.
       (COND c a F = c /\ a) /\ (COND c a T = ~c \/ a) /\
       (COND c T b = c \/ b) /\ (COND c F b = ~c /\ b)``,
   RW_TAC std_ss [IMP_DISJ_THM]);

val () = computeLib.add_funs [EXISTS_COND, COND_SIMP];

(******************************************************************************
* Examples
******************************************************************************)

(* 
** Generated this from a Verilog model of the BUF example in
** Chapter 4 of FoCs User's Manual (see test2.v)
** but with each component separately clocked
** (www.haifa.il.ibm.com/projects/verification/focs/)
*)

val clk1_def     = Define `clk1     = 1`;
val clk2_def     = Define `clk2     = 2`;
val clk3_def     = Define `clk3     = 3`;
val StoB_REQ_def = Define `StoB_REQ = 4`;
val BtoS_ACK_def = Define `BtoS_ACK = 5`;
val BtoR_REQ_def = Define `BtoR_REQ = 6`;
val RtoB_ACK_def = Define `RtoB_ACK = 7`;


quietdec := true; 
val SimRun_def =
 Define
  `SimRun =
      [{}; 
       {}; 
       {}; 
       {}; 
       {clk1}; 
       {clk1; clk2}; 
       {clk2; StoB_REQ};
       {clk2; clk3; StoB_REQ}; 
       {clk3; StoB_REQ}; 
       {clk1; clk3; StoB_REQ};
       {clk1; clk2; clk3; StoB_REQ}; 
       {clk2; clk3; StoB_REQ};
       {clk2; StoB_REQ}; 
       {clk2; StoB_REQ; BtoS_ACK}; 
       {StoB_REQ; BtoS_ACK};
       {clk1; StoB_REQ; BtoS_ACK}; 
       {clk1; BtoS_ACK}; 
       {clk1; clk3; BtoS_ACK};
       {clk1; clk2; clk3; BtoS_ACK}; 
       {clk2; clk3; BtoS_ACK};
       {clk2; clk3; BtoS_ACK; BtoR_REQ};
       {clk1; clk2; clk3; BtoS_ACK; BtoR_REQ};
       {clk1; clk3; BtoS_ACK; BtoR_REQ}; 
       {clk1; BtoS_ACK; BtoR_REQ};
       {BtoS_ACK; BtoR_REQ}; 
       {clk2; BtoS_ACK; BtoR_REQ};
       {clk2; BtoS_ACK; BtoR_REQ; RtoB_ACK};
       {clk1; clk2; BtoS_ACK; BtoR_REQ; RtoB_ACK};
       {clk1; clk2; clk3; BtoS_ACK; BtoR_REQ; RtoB_ACK};
       {clk1; clk3; BtoS_ACK; BtoR_REQ; RtoB_ACK};
       {clk1; clk3; BtoS_ACK; RtoB_ACK}; 
       {clk3; BtoS_ACK; RtoB_ACK};
       {clk2; clk3; BtoS_ACK; RtoB_ACK}; 
       {clk2; clk3}; 
       {clk2}; 
       {clk1; clk2};
       {clk1}; 
       {}; 
       {clk3}; 
       {clk2; clk3}; 
       {clk1; clk2; clk3};
       {clk2; clk3; StoB_REQ}; 
       {clk3; StoB_REQ}; 
       {StoB_REQ};
       {clk1; StoB_REQ}; 
       {clk1; clk2; StoB_REQ}; 
       {clk2; clk3; StoB_REQ};
       {clk2; clk3; StoB_REQ; BtoS_ACK}; 
       {clk3; StoB_REQ; BtoS_ACK};
       {clk1; clk3; StoB_REQ; BtoS_ACK}; 
       {clk1; clk3; BtoS_ACK};
       {clk1; clk2; clk3; BtoS_ACK}; 
       {clk1; clk2; BtoS_ACK};
       {clk2; BtoS_ACK}; 
       {clk2; BtoS_ACK; BtoR_REQ}; 
       {BtoS_ACK; BtoR_REQ};
       {clk1; BtoS_ACK; BtoR_REQ}; 
       {clk1; clk3; BtoS_ACK; BtoR_REQ};
       {clk1; clk2; clk3; BtoS_ACK; BtoR_REQ};
       {clk2; clk3; BtoS_ACK; BtoR_REQ};
       {clk2; clk3; BtoS_ACK; BtoR_REQ; RtoB_ACK};
       {clk1; clk3; BtoS_ACK; BtoR_REQ; RtoB_ACK};
       {clk1; BtoS_ACK; RtoB_ACK}; 
       {clk2; BtoS_ACK; RtoB_ACK}; 
       {clk2};
       {clk2; clk3}; 
       {clk1; clk2; clk3}; 
       {clk1; clk3}; 
       {clk3}; 
       {clk2; clk3};
       {clk2}; 
       {clk1; clk2}; 
       {clk1}; 
       {StoB_REQ}; 
       {clk3; StoB_REQ};
       {clk2; clk3; StoB_REQ}; 
       {clk1; clk2; clk3; StoB_REQ};
       {clk1; clk2; clk3; StoB_REQ; BtoS_ACK}; 
       {clk1; StoB_REQ; BtoS_ACK};
       {StoB_REQ; BtoS_ACK}; 
       {BtoS_ACK}; 
       {clk2; BtoS_ACK};
       {clk1; clk2; BtoS_ACK}; 
       {clk1; clk2; clk3; BtoS_ACK; BtoR_REQ};
       {clk2; clk3; BtoS_ACK; BtoR_REQ}; 
       {clk3; BtoS_ACK; BtoR_REQ};
       {clk1; clk3; BtoS_ACK; BtoR_REQ};
       {clk1; clk2; clk3; BtoS_ACK; BtoR_REQ};
       {clk1; clk2; BtoS_ACK; BtoR_REQ};
       {clk1; clk2; BtoS_ACK; BtoR_REQ; RtoB_ACK};
       {clk2; BtoS_ACK; BtoR_REQ; RtoB_ACK}; 
       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
       {BtoS_ACK; RtoB_ACK}; 
       {clk1; clk3; BtoS_ACK; RtoB_ACK};
       {clk1; clk2; clk3; BtoS_ACK; RtoB_ACK}; 
       {clk1; clk2; clk3};
       {clk2; clk3}; 
       {clk2}; 
       {}; 
       {clk1}; 
       {clk1; clk2}; 
       {clk2; StoB_REQ};
       {clk2; clk3; StoB_REQ}; 
       {clk1; clk2; clk3; StoB_REQ};
       {clk1; clk3; StoB_REQ}; 
       {clk3; StoB_REQ}; 
       {clk2; StoB_REQ};
       {clk1; clk2; StoB_REQ}; 
       {clk1; clk2; StoB_REQ; BtoS_ACK};
       {clk1; StoB_REQ; BtoS_ACK}; 
       {clk1; clk3; StoB_REQ; BtoS_ACK};
       {clk3; StoB_REQ; BtoS_ACK}; 
       {clk3; BtoS_ACK}; 
       {clk2; clk3; BtoS_ACK};
       {clk1; clk2; clk3; BtoS_ACK}; 
       {clk1; clk2; clk3; BtoS_ACK; BtoR_REQ};
       {clk1; clk2; BtoS_ACK; BtoR_REQ}; 
       {clk1; BtoS_ACK; BtoR_REQ};
       {BtoS_ACK; BtoR_REQ}; 
       {clk2; BtoS_ACK; BtoR_REQ};
       {clk1; clk2; BtoS_ACK; BtoR_REQ};
       {clk1; clk2; BtoS_ACK; BtoR_REQ; RtoB_ACK};
       {clk1; clk2; clk3; BtoS_ACK; BtoR_REQ; RtoB_ACK};
       {clk3; BtoS_ACK; BtoR_REQ; RtoB_ACK}; 
       {clk3; BtoS_ACK; RtoB_ACK};
       {BtoS_ACK; RtoB_ACK}; 
       {clk1; clk2; BtoS_ACK; RtoB_ACK}; 
       {clk1; clk2};
       {clk2}; 
       {}; 
       {clk3}; 
       {clk1; clk3}; 
       {clk1; clk2; clk3};
       {clk2; clk3; StoB_REQ}; 
       {clk2; StoB_REQ}; 
       {StoB_REQ};
       {clk1; StoB_REQ}; 
       {clk1; clk2; StoB_REQ}; 
       {clk2; clk3; StoB_REQ};
       {clk2; clk3; StoB_REQ; BtoS_ACK}; 
       {clk3; StoB_REQ; BtoS_ACK};
       {clk1; clk3; StoB_REQ; BtoS_ACK}; 
       {clk1; clk3; BtoS_ACK};
       {clk1; BtoS_ACK}; 
       {clk1; clk2; BtoS_ACK}; 
       {clk2; BtoS_ACK};
       {clk2; BtoS_ACK; BtoR_REQ}; 
       {clk1; clk2; BtoS_ACK; BtoR_REQ};
       {clk1; BtoS_ACK; BtoR_REQ}; 
       {clk1; clk3; BtoS_ACK; BtoR_REQ};
       {clk3; BtoS_ACK; BtoR_REQ}; 
       {clk2; clk3; BtoS_ACK; BtoR_REQ};
       {clk2; clk3; BtoS_ACK; BtoR_REQ; RtoB_ACK};
       {clk1; clk2; clk3; BtoS_ACK; BtoR_REQ; RtoB_ACK};
       {clk1; clk2; BtoS_ACK; BtoR_REQ; RtoB_ACK};
       {clk1; BtoS_ACK; BtoR_REQ; RtoB_ACK}; 
       {clk1; BtoS_ACK; RtoB_ACK};
       {BtoS_ACK; RtoB_ACK}; 
       {clk2; BtoS_ACK; RtoB_ACK}; 
       {clk2};
       {clk2; clk3}; 
       {clk1; clk2; clk3}; 
       {clk1; clk3}; 
       {clk3}; 
       {}; 
       {clk2};
       {clk1; clk2}; 
       {clk2; StoB_REQ}; 
       {StoB_REQ}; 
       {clk3; StoB_REQ};
       {clk1; clk3; StoB_REQ}; 
       {clk1; clk2; clk3; StoB_REQ};
       {clk1; clk2; StoB_REQ}; 
       {clk2; StoB_REQ}; 
       {clk2; StoB_REQ; BtoS_ACK};
       {StoB_REQ; BtoS_ACK}; 
       {clk1; StoB_REQ; BtoS_ACK}; 
       {clk1; BtoS_ACK};
       {clk1; clk2; BtoS_ACK}; 
       {clk1; clk2; clk3; BtoS_ACK};
       {clk2; clk3; BtoS_ACK}; 
       {clk2; clk3; BtoS_ACK; BtoR_REQ};
       {clk3; BtoS_ACK; BtoR_REQ}; 
       {clk1; clk3; BtoS_ACK; BtoR_REQ};
       {clk1; BtoS_ACK; BtoR_REQ}; 
       {clk1; clk2; BtoS_ACK; BtoR_REQ};
       {clk2; BtoS_ACK; BtoR_REQ}; 
       {clk2; BtoS_ACK; BtoR_REQ; RtoB_ACK};
       {clk1; clk3; BtoS_ACK; BtoR_REQ; RtoB_ACK};
       {clk1; clk3; BtoS_ACK; RtoB_ACK}; 
       {clk2; clk3; BtoS_ACK; RtoB_ACK};
       {clk2; clk3}; 
       {clk2}; 
       {clk1; clk2}; 
       {clk1}; 
       {}; 
       {clk2}; 
       {clk2; clk3};
       {clk1; clk2; clk3}; 
       {clk1; clk3}; 
       {clk3; StoB_REQ}; 
       {StoB_REQ};
       {clk2; StoB_REQ}; 
       {clk1; clk2; StoB_REQ};
       {clk1; clk2; StoB_REQ; BtoS_ACK};
       {clk1; clk2; clk3; StoB_REQ; BtoS_ACK};
       {clk1; clk3; StoB_REQ; BtoS_ACK}; 
       {clk3; StoB_REQ; BtoS_ACK};
       {clk3; BtoS_ACK}; 
       {clk2; clk3; BtoS_ACK};
       {clk1; clk2; clk3; BtoS_ACK}; 
       {clk1; clk2; BtoS_ACK};
       {clk1; clk2; BtoS_ACK; BtoR_REQ}; 
       {clk2; BtoS_ACK; BtoR_REQ};
       {BtoS_ACK; BtoR_REQ}; 
       {clk1; BtoS_ACK; BtoR_REQ};
       {clk1; clk2; clk3; BtoS_ACK; BtoR_REQ};
       {clk1; clk2; clk3; BtoS_ACK; BtoR_REQ; RtoB_ACK};
       {clk2; clk3; BtoS_ACK; BtoR_REQ; RtoB_ACK};
       {clk3; BtoS_ACK; BtoR_REQ; RtoB_ACK}; 
       {clk3; BtoS_ACK; RtoB_ACK};
       {BtoS_ACK; RtoB_ACK}; 
       {clk1; BtoS_ACK; RtoB_ACK};
       {clk1; clk2; BtoS_ACK; RtoB_ACK}; 
       {clk1; clk2}; 
       {clk2}; 
       {clk2; clk3};
       {clk3}; 
       {clk1; clk3}; 
       {clk1; clk2; clk3}; 
       {clk2; clk3; StoB_REQ};
       {clk2; StoB_REQ}; 
       {clk1; clk2; StoB_REQ}; 
       {clk1; StoB_REQ};
       {clk3; StoB_REQ}; 
       {clk2; clk3; StoB_REQ};
       {clk1; clk2; clk3; StoB_REQ}; 
       {clk1; clk2; clk3; StoB_REQ; BtoS_ACK};
       {clk1; clk3; StoB_REQ; BtoS_ACK}; 
       {clk1; StoB_REQ; BtoS_ACK};
       {StoB_REQ; BtoS_ACK}; 
       {BtoS_ACK}; 
       {clk2; BtoS_ACK};
       {clk1; clk2; BtoS_ACK}; 
       {clk1; clk2; BtoS_ACK; BtoR_REQ};
       {clk1; clk2; clk3; BtoS_ACK; BtoR_REQ};
       {clk1; clk3; BtoS_ACK; BtoR_REQ}; 
       {clk3; BtoS_ACK; BtoR_REQ};
       {clk2; clk3; BtoS_ACK; BtoR_REQ};
       {clk1; clk2; clk3; BtoS_ACK; BtoR_REQ};
       {clk1; clk2; BtoS_ACK; BtoR_REQ; RtoB_ACK};
       {BtoS_ACK; BtoR_REQ; RtoB_ACK}; 
       {BtoS_ACK; RtoB_ACK};
       {clk3; BtoS_ACK; RtoB_ACK}; 
       {clk1; clk2; clk3; BtoS_ACK; RtoB_ACK};
       {clk1; clk2; clk3}; 
       {clk2; clk3}; 
       {clk3}; 
       {}; 
       {clk1}; 
       {clk1; clk2};
       {clk2; StoB_REQ}; 
       {clk2; clk3; StoB_REQ}; 
       {clk3; StoB_REQ};
       {clk1; clk3; StoB_REQ}; 
       {clk1; clk2; clk3; StoB_REQ};
       {clk1; clk2; StoB_REQ}; 
       {clk2; StoB_REQ}; 
       {clk2; StoB_REQ; BtoS_ACK};
       {StoB_REQ; BtoS_ACK}; 
       {clk1; StoB_REQ; BtoS_ACK};
       {clk1; clk3; BtoS_ACK}; 
       {clk1; clk2; clk3; BtoS_ACK};
       {clk2; clk3; BtoS_ACK}; 
       {clk2; clk3; BtoS_ACK; BtoR_REQ};
       {clk1; clk2; clk3; BtoS_ACK; BtoR_REQ};
       {clk1; clk3; BtoS_ACK; BtoR_REQ}; 
       {clk1; BtoS_ACK; BtoR_REQ};
       {BtoS_ACK; BtoR_REQ}; 
       {clk2; BtoS_ACK; BtoR_REQ};
       {clk2; BtoS_ACK; BtoR_REQ; RtoB_ACK};
       {clk1; clk2; clk3; BtoS_ACK; BtoR_REQ; RtoB_ACK};
       {clk1; clk3; BtoS_ACK; BtoR_REQ; RtoB_ACK};
       {clk1; clk3; BtoS_ACK; RtoB_ACK}; 
       {clk3; BtoS_ACK; RtoB_ACK};
       {clk2; clk3; BtoS_ACK; RtoB_ACK}; 
       {clk2; clk3}; 
       {clk2}; 
       {clk1; clk2};
       {clk1}; 
       {}; 
       {clk3}; 
       {clk2; clk3}; 
       {clk1; clk2; clk3};
       {clk2; clk3; StoB_REQ}; 
       {StoB_REQ}; 
       {clk1; StoB_REQ};
       {clk1; clk2; StoB_REQ}; 
       {clk1; clk2; clk3; StoB_REQ};
       {clk2; clk3; StoB_REQ}; 
       {clk2; clk3; StoB_REQ; BtoS_ACK};
       {clk3; StoB_REQ; BtoS_ACK}; 
       {clk1; clk3; StoB_REQ; BtoS_ACK};
       {clk1; clk3; BtoS_ACK}; 
       {clk1; clk2; clk3; BtoS_ACK};
       {clk1; clk2; BtoS_ACK}; 
       {clk2; BtoS_ACK}; 
       {clk2; BtoS_ACK; BtoR_REQ};
       {BtoS_ACK; BtoR_REQ}; 
       {clk1; BtoS_ACK; BtoR_REQ};
       {clk1; clk3; BtoS_ACK; BtoR_REQ};
       {clk1; clk2; clk3; BtoS_ACK; BtoR_REQ};
       {clk2; clk3; BtoS_ACK; BtoR_REQ};
       {clk2; clk3; BtoS_ACK; BtoR_REQ; RtoB_ACK};
       {clk2; BtoS_ACK; BtoR_REQ; RtoB_ACK};
       {clk1; BtoS_ACK; BtoR_REQ; RtoB_ACK}; 
       {clk1; BtoS_ACK; RtoB_ACK};
       {clk2; BtoS_ACK; RtoB_ACK}; 
       {clk2}; 
       {clk2; clk3}; 
       {clk1; clk2; clk3};
       {clk1; clk3}; 
       {clk3}; 
       {clk2}; 
       {clk1; clk2}; 
       {clk1}; 
       {clk3};
       {clk2; clk3}]`;
quietdec := false;

(* A pure computeLib version *)
time
 EVAL
 ``US_SEM
    SimRun
    (S_CAT(S_REPEAT S_TRUE,
           S_CAT(S_BOOL(B_PROP StoB_REQ), 
                 S_REPEAT S_TRUE)))``;

(* A version using BIGLIST to keep terms small
   (however, it doesn't seem to have much effect)
val SimRun_def = pureDefine `SimRun = SimRun`;
val () = computeLib.add_funs (time EVAL_BIGLIST SimRun_def);
time
 EVAL
 ``US_SEM
    (BIGLIST SimRun)
    (S_CAT(S_REPEAT S_TRUE,
           S_CAT(S_BOOL(B_PROP StoB_REQ), 
                 S_REPEAT S_TRUE)))``;
*)

time
 EVAL 
 ``US_SEM 
    SimRun
    (S_CAT(S_REPEAT S_TRUE, 
           S_CAT(S_CAT(S_BOOL(B_PROP StoB_REQ),S_BOOL(B_PROP StoB_REQ)),
                 S_REPEAT S_TRUE)))``;

time
 EVAL 
 ``US_SEM 
    SimRun
    (S_CAT(S_REPEAT S_TRUE, 
           S_CAT(S_CAT(S_BOOL(B_PROP StoB_REQ),S_BOOL(B_PROP BtoR_REQ)),
                 S_REPEAT S_TRUE)))``;

(******************************************************************************
* The following 4 properties make up the vunit
* four_phase_handshake_left of page 19 of the FoCs User's Manual
* with "never r" replaced by "{r}(F)"
******************************************************************************)

(*  
** {[*]; !StoB_REQ & BtoS_ACK; StoB_REQ}(F)  
*)
time
 EVAL
 ``UF_SEM
    (FINITE SimRun)
    (F_SUFFIX_IMP
      (S_CAT(S_REPEAT S_TRUE, 
             S_CAT(S_BOOL(B_AND(B_NOT(B_PROP StoB_REQ), B_PROP BtoS_ACK)),
                   S_BOOL(B_PROP StoB_REQ))),
       F_BOOL B_FALSE))``;

(*  
** {[*]; StoB_REG & !BtoS_ACK; !StoB_REQ}(F)  
*)
time
 EVAL
 ``UF_SEM
    (FINITE SimRun)
    (F_SUFFIX_IMP
      (S_CAT(S_REPEAT S_TRUE, 
             S_CAT(S_BOOL(B_AND(B_PROP StoB_REQ, B_NOT(B_PROP BtoS_ACK))),
                   S_BOOL(B_NOT(B_PROP StoB_REQ)))),
       F_BOOL B_FALSE))``;

(*  
** {[*]; !BtoS_ACK & !StoB_REQ; BtoS_ACK}(F)  
*)
time
 EVAL
 ``UF_SEM
    (FINITE SimRun)
    (F_SUFFIX_IMP
      (S_CAT(S_REPEAT S_TRUE, 
             S_CAT(S_BOOL(B_AND(B_NOT(B_PROP BtoS_ACK), B_NOT(B_PROP StoB_REQ))),
                   S_BOOL(B_PROP BtoS_ACK))),
       F_BOOL B_FALSE))``;

(*  
** {[*]; BtoS_ACK & StoB_REQ; !BtoS_ACK}(F)  
*)
time
 EVAL
 ``UF_SEM
    (FINITE SimRun)
    (F_SUFFIX_IMP
      (S_CAT(S_REPEAT S_TRUE, 
             S_CAT(S_BOOL(B_AND(B_PROP BtoS_ACK, B_PROP StoB_REQ)),
                   S_BOOL(B_NOT(B_PROP BtoS_ACK)))),
       F_BOOL B_FALSE))``;


(******************************************************************************
* Make "&" into an infix for F_AND
******************************************************************************)
val _ = set_fixity "&" (Infixl 500);
val F_AND_IX_def = xDefine "F_AND_IX" `$& f1 f2 = F_AND(f1,f2)`;

(******************************************************************************
* A single property characterising a four-phasse handshake
******************************************************************************)

val FOUR_PHASE_def =
 Define
  `FOUR_PHASE req ack =
    F_SUFFIX_IMP
     (S_CAT(S_REPEAT S_TRUE, 
            S_CAT(S_BOOL(B_AND(B_NOT(B_PROP req), B_PROP ack)),
                  S_BOOL(B_PROP req))),
      F_BOOL B_FALSE)
    &
    F_SUFFIX_IMP
     (S_CAT(S_REPEAT S_TRUE, 
            S_CAT(S_BOOL(B_AND(B_PROP req, B_NOT(B_PROP ack))),
                  S_BOOL(B_NOT(B_PROP req)))),
      F_BOOL B_FALSE)
    &  
    F_SUFFIX_IMP
     (S_CAT(S_REPEAT S_TRUE, 
            S_CAT(S_BOOL(B_AND(B_NOT(B_PROP ack), B_NOT(B_PROP req))),
                  S_BOOL(B_PROP ack))),
      F_BOOL B_FALSE)
    &
    F_SUFFIX_IMP
     (S_CAT(S_REPEAT S_TRUE, 
            S_CAT(S_BOOL(B_AND(B_PROP ack, B_PROP req)),
                  S_BOOL(B_NOT(B_PROP ack)))),
      F_BOOL B_FALSE)`;

(*  
** vunit four_phase_handskake_left (page 19, FoCs User's Manual)
** FOUR_PHASE StoB_REQ BtoS_ACK
*)

time EVAL ``UF_SEM (FINITE SimRun) (FOUR_PHASE StoB_REQ BtoS_ACK)``;


(*  
** vunit four_phase_handskake_right (page 20, FoCs User's Manual)
** FOUR_PHASE BtoR_REQ RtoB_ACK
*)

time EVAL ``UF_SEM (FINITE SimRun) (FOUR_PHASE BtoR_REQ RtoB_ACK)``;

(******************************************************************************
* f1 before f2 = [not f2 W (f1 & not f2)]
******************************************************************************)
val F_BEFORE_def =
 Define
  `F_BEFORE(f1,f2) = F_W(F_NOT f2, F_AND(f1, F_NOT f2))`;

(*  
** SimRun |= StoB_REQ before BtoS_ACK
*)
time
 EVAL
 ``UF_SEM
    (FINITE SimRun)
    (F_BEFORE(F_BOOL(B_PROP StoB_REQ), F_BOOL(B_PROP BtoS_ACK)))``;

(*  
** SimRun |= BtoS_ACK before StoB_REQ
*)
time
 EVAL
 ``UF_SEM
    (FINITE SimRun)
    (F_BEFORE(F_BOOL(B_PROP BtoS_ACK), F_BOOL(B_PROP StoB_REQ)))``;

(*  
** SimRun |= {[*]}(StoB_REQ before BtoS_ACK)
*)
time
 EVAL
 ``UF_SEM
    (FINITE SimRun)
    (F_SUFFIX_IMP
     (S_REPEAT S_TRUE, 
      F_BEFORE(F_BOOL(B_PROP StoB_REQ), F_BOOL(B_PROP BtoS_ACK))))``;

(*  
** SimRun |= {[*]}(BtoS_ACK before StoB_REQ)
*)
time
 EVAL
 ``UF_SEM
    (FINITE SimRun)
    (F_SUFFIX_IMP
     (S_REPEAT S_TRUE, 
      F_BEFORE(F_BOOL(B_PROP BtoS_ACK), F_BOOL(B_PROP StoB_REQ))))``;


(******************************************************************************
* Make ";;" into an infix for S_CAT
******************************************************************************)
val _ = set_fixity ";;" (Infixl 500);
val S_CAT_IX_def = xDefine "S_CAT_IX" `$;; r1 r2 = S_CAT(r1,r2)`;

(******************************************************************************
* SimRun |= {[*];!BtoS_ACK;BtoS_ACK}(F)
******************************************************************************)
time
 EVAL
 ``UF_SEM
    (FINITE SimRun)
    (F_SUFFIX_IMP
     ((S_REPEAT(S_BOOL B_TRUE) ;;
       S_BOOL(B_NOT(B_PROP BtoS_ACK)) ;; 
       S_BOOL(B_PROP BtoS_ACK)),
      F_BOOL B_FALSE))``;

(******************************************************************************
* SimRun |= {[*];!BtoS_ACK;BtoS_ACK;[*];!BtoS_ACK;BtoS_ACK}(F)
******************************************************************************)
time
 EVAL
 ``UF_SEM
    (FINITE SimRun)
    (F_SUFFIX_IMP
     ((S_REPEAT(S_BOOL B_TRUE) ;;
       S_BOOL(B_NOT(B_PROP BtoS_ACK)) ;; 
       S_BOOL(B_PROP BtoS_ACK) ;;
       S_REPEAT(S_BOOL B_TRUE) ;;
       S_BOOL(B_NOT(B_PROP BtoS_ACK)) ;; 
       S_BOOL(B_PROP BtoS_ACK)),
      F_BOOL B_FALSE))``;

(******************************************************************************
* SimRun |= {[*];BtoS_ACK;[RtoB_ACK];BtoS_ACK}(F)
******************************************************************************)
time
 EVAL
 ``UF_SEM
    (FINITE SimRun)
    (F_SUFFIX_IMP
     ((S_REPEAT(S_BOOL B_TRUE) ;;
       S_BOOL(B_PROP BtoS_ACK) ;;
       S_REPEAT(S_BOOL(B_PROP RtoB_ACK)) ;;
       S_BOOL(B_PROP BtoS_ACK)),
      F_BOOL B_FALSE))``;

(******************************************************************************
* SimRun |= {[*];!BtoS_ACK;BtoS_ACK;[RtoB_ACK];!BtoS_ACK;BtoS_ACK}(F)
******************************************************************************)
time
 EVAL
 ``UF_SEM
    (FINITE SimRun)
    (F_SUFFIX_IMP
     ((S_REPEAT(S_BOOL B_TRUE) ;;
       S_BOOL(B_NOT(B_PROP BtoS_ACK)) ;; 
       S_BOOL(B_PROP BtoS_ACK) ;;
       S_REPEAT(S_BOOL(B_PROP RtoB_ACK)) ;;
       S_BOOL(B_NOT(B_PROP BtoS_ACK)) ;; 
       S_BOOL(B_PROP BtoS_ACK)),
      F_BOOL B_FALSE))``;

(******************************************************************************
* SimRun |= {[*];BtoS_ACK;[!RtoB_ACK];BtoS_ACK}(F)
******************************************************************************)
time
 EVAL
 ``UF_SEM
    (FINITE SimRun)
    (F_SUFFIX_IMP
     ((S_REPEAT(S_BOOL B_TRUE) ;;
       S_BOOL(B_PROP BtoS_ACK) ;;
       S_REPEAT(S_BOOL(B_NOT(B_PROP RtoB_ACK))) ;;
       S_BOOL(B_PROP BtoS_ACK)),
      F_BOOL B_FALSE))``;

(******************************************************************************
* SimRun |= {[*];!BtoS_ACK;BtoS_ACK;[!RtoB_ACK];!BtoS_ACK;BtoS_ACK}(F)
******************************************************************************)
time
 EVAL
 ``UF_SEM
    (FINITE SimRun)
    (F_SUFFIX_IMP
     ((S_REPEAT(S_BOOL B_TRUE) ;;
       S_BOOL(B_NOT(B_PROP BtoS_ACK)) ;; 
       S_BOOL(B_PROP BtoS_ACK) ;;
       S_REPEAT(S_BOOL(B_NOT(B_PROP RtoB_ACK))) ;;
       S_BOOL(B_NOT(B_PROP BtoS_ACK)) ;; 
       S_BOOL(B_PROP BtoS_ACK)),
      F_BOOL B_FALSE))``;

(******************************************************************************
* SimRun 
*  |= {[*];!BtoS_ACK;BtoS_ACK;[*];!RtoB_ACK;RtoB_ACK;[*];!BtoS_ACK;BtoS_ACK}(F)
******************************************************************************)
time
 EVAL
 ``UF_SEM
    (FINITE SimRun)
    (F_SUFFIX_IMP
     ((S_REPEAT(S_BOOL B_TRUE) ;;
       S_BOOL(B_NOT(B_PROP BtoS_ACK)) ;; 
       S_BOOL(B_PROP BtoS_ACK) ;;
       S_REPEAT(S_BOOL(B_TRUE)) ;;
       S_BOOL(B_NOT(B_PROP RtoB_ACK)) ;;
       S_BOOL(B_PROP RtoB_ACK) ;;
       S_REPEAT(S_BOOL(B_TRUE)) ;;
       S_BOOL(B_NOT(B_PROP BtoS_ACK)) ;; 
       S_BOOL(B_PROP BtoS_ACK)),
      F_BOOL B_FALSE))``;

(******************************************************************************
* SimRun 
*  |= {[*];!BtoS_ACK;BtoS_ACK;
*          [BtoS_ACK];[!BtoS_ACK];
*          ((!RtoB_ACK;RtoB_ACK;)&&(!BtoS_ACK;!BtoS_ACK));
*          [!BtoS_ACK];BtoS_ACK}
******************************************************************************)
time
 EVAL
 ``US_SEM
    SimRun
      ((S_REPEAT(S_BOOL B_TRUE) ;;
        S_BOOL(B_NOT(B_PROP BtoS_ACK)) ;; 
        S_BOOL(B_PROP BtoS_ACK) ;;
        S_REPEAT(S_BOOL(B_PROP BtoS_ACK));;
        S_REPEAT(S_BOOL(B_NOT(B_PROP BtoS_ACK)));;
        S_AND((S_BOOL(B_NOT(B_PROP RtoB_ACK)) ;; S_BOOL(B_PROP RtoB_ACK)),
              (S_BOOL(B_NOT(B_PROP BtoS_ACK)) ;; S_BOOL(B_NOT(B_PROP BtoS_ACK)))) ;;
        S_REPEAT(S_BOOL(B_NOT(B_PROP BtoS_ACK)));;
        S_BOOL(B_PROP BtoS_ACK)))``;
 
(******************************************************************************
* SimRun 
*  |= {[*];!BtoS_ACK;BtoS_ACK;
*          [BtoS_ACK];[!BtoS_ACK];
*          ((!RtoB_ACK;RtoB_ACK;)&&(!BtoS_ACK;!BtoS_ACK));
*          [!BtoS_ACK];BtoS_ACK}
*     (F)
******************************************************************************)
time
 EVAL
 ``UF_SEM
    (FINITE SimRun)
    (F_SUFFIX_IMP
     ((S_REPEAT(S_BOOL B_TRUE) ;;
       S_BOOL(B_NOT(B_PROP BtoS_ACK)) ;; 
       S_BOOL(B_PROP BtoS_ACK) ;;
       S_REPEAT(S_BOOL(B_PROP BtoS_ACK));;
       S_REPEAT(S_BOOL(B_NOT(B_PROP BtoS_ACK)));;
       S_AND((S_BOOL(B_NOT(B_PROP RtoB_ACK)) ;; S_BOOL(B_PROP RtoB_ACK)),
             (S_BOOL(B_NOT(B_PROP BtoS_ACK)) ;; S_BOOL(B_NOT(B_PROP BtoS_ACK)))) ;;
       S_REPEAT(S_BOOL(B_NOT(B_PROP BtoS_ACK)));;
       S_BOOL(B_PROP BtoS_ACK)),
      F_BOOL B_FALSE))``;

(******************************************************************************
* SimRun 
*  |= {[*];!BtoS_ACK;BtoS_ACK;
*          [BtoS_ACK];[!BtoS_ACK];
*          ((!RtoB_ACK;RtoB_ACK;)&&(!BtoS_ACK;!BtoS_ACK));
*          [!BtoS_ACK];BtoS_ACK}
*     (T)
******************************************************************************)
time
 EVAL
 ``UF_SEM
    (FINITE SimRun)
    (F_SUFFIX_IMP
     ((S_REPEAT(S_BOOL B_TRUE) ;;
       S_BOOL(B_NOT(B_PROP BtoS_ACK)) ;; 
       S_BOOL(B_PROP BtoS_ACK) ;;
       S_REPEAT(S_BOOL(B_PROP BtoS_ACK));;
       S_REPEAT(S_BOOL(B_NOT(B_PROP BtoS_ACK)));;
       S_AND((S_BOOL(B_NOT(B_PROP RtoB_ACK)) ;; S_BOOL(B_PROP RtoB_ACK)),
             (S_BOOL(B_NOT(B_PROP BtoS_ACK)) ;; S_BOOL(B_NOT(B_PROP BtoS_ACK)))) ;;
       S_REPEAT(S_BOOL(B_NOT(B_PROP BtoS_ACK)));;
       S_BOOL(B_PROP BtoS_ACK)),
      F_BOOL B_TRUE))``;
(******************************************************************************
* SimRun 
*  |= {[*];!BtoS_ACK;
*          BtoS_ACK;
*          [BtoS_ACK&!RtoB_ACK];
*          [!BtoS_ACK&!RoB_ACK];
*          BtoS_ACK}
*     (F)
******************************************************************************)
time
 EVAL
 ``UF_SEM
    (FINITE SimRun)
    (F_SUFFIX_IMP
     ((S_REPEAT(S_BOOL B_TRUE) ;;
       S_BOOL(B_NOT(B_PROP BtoS_ACK)) ;; 
       S_BOOL(B_PROP BtoS_ACK) ;;
       S_REPEAT(S_BOOL(B_AND(B_PROP BtoS_ACK,
                             B_NOT(B_PROP RtoB_ACK)))) ;;
       S_REPEAT(S_BOOL(B_AND(B_NOT(B_PROP BtoS_ACK),
                             B_NOT(B_PROP RtoB_ACK)))) ;;
       S_BOOL(B_PROP BtoS_ACK)),
      F_BOOL B_FALSE))``;

(******************************************************************************
* SimRun 
*  |= {[*]; !BtoS_ACK; BtoS_ACK; true}
*     ((!RtoB_ACK & X RtoB_ACK) before (!BtoS_ACK & X BtoS_ACK))
******************************************************************************)
time
 EVAL
 ``UF_SEM
    (FINITE SimRun)
    (F_SUFFIX_IMP
     ((S_REPEAT(S_BOOL B_TRUE) ;;
       S_BOOL(B_NOT(B_PROP BtoS_ACK)) ;; 
       S_BOOL(B_PROP BtoS_ACK) ;;
       S_BOOL B_TRUE),
      F_BEFORE
       (F_AND(F_NOT(F_BOOL(B_PROP RtoB_ACK)), 
              F_NEXT(F_BOOL(B_PROP RtoB_ACK))),
        F_AND(F_NOT(F_BOOL(B_PROP BtoS_ACK)), 
              F_NEXT(F_BOOL(B_PROP BtoS_ACK))))))``;

(******************************************************************************
* SimRun 
*  |= {[*]; !RtoB_ACK; RtoB_ACK; true}
*     ((!BtoS_ACK & X BtoS_ACK) before (!RtoB_ACK & X RtoB_ACK))
******************************************************************************)
time
 EVAL
 ``UF_SEM
    (FINITE SimRun)
    (F_SUFFIX_IMP
     ((S_REPEAT(S_BOOL B_TRUE) ;;
       S_BOOL(B_NOT(B_PROP BtoS_ACK)) ;; 
       S_BOOL(B_PROP BtoS_ACK) ;;
       S_BOOL B_TRUE),
      F_BEFORE
       (F_AND(F_NOT(F_BOOL(B_PROP RtoB_ACK)), 
              F_NEXT(F_BOOL(B_PROP RtoB_ACK))),
        F_AND(F_NOT(F_BOOL(B_PROP BtoS_ACK)), 
              F_NEXT(F_BOOL(B_PROP BtoS_ACK))))))``;



(******************************************************************************
* SimRun 
*  |= (!BtoS_ACK & X BtoS_ACK) before (!RtoB_ACK & X RtoB_ACK)
******************************************************************************)
time
 EVAL
 ``UF_SEM
    (FINITE SimRun)
    (F_BEFORE
       (F_AND(F_NOT(F_BOOL(B_PROP RtoB_ACK)), 
              F_NEXT(F_BOOL(B_PROP RtoB_ACK))),
        F_AND(F_NOT(F_BOOL(B_PROP BtoS_ACK)), 
              F_NEXT(F_BOOL(B_PROP BtoS_ACK)))))``;

(******************************************************************************
* Some examples using EVAL to perform clock removing rewriting used in paper
******************************************************************************)
time
 EVAL 
 ``S_CLOCK_COMP c 
    (S_CAT(S_REPEAT S_TRUE, 
           S_CAT(S_AND(S_BOOL(B_NOT(B_PROP rq)), S_BOOL(B_PROP ak)), 
                 S_BOOL(B_PROP rq))))``;


time
 EVAL 
 ``S_CLOCK_COMP c1 
    (S_CAT(S_REPEAT S_TRUE, 
           S_CAT(S_AND(S_BOOL(B_NOT(B_PROP rq)), S_CLOCK(S_BOOL(B_PROP ak),B_PROP c2)), 
                 S_BOOL(B_PROP rq))))``;

time
 EVAL
 ``S_CLOCK_COMP c 
    (S_CAT(S_REPEAT S_TRUE, 
           S_CAT(S_AND(S_CLOCK(S_BOOL(B_NOT(B_PROP rq)),B_PROP c1), 
                       S_CLOCK(S_BOOL(B_PROP ak),B_PROP c2)), 
                 S_CLOCK(S_BOOL(B_PROP rq), B_PROP c1))))``;;

time
 (REWRITE_RULE[S_CAT_IX_def] o EVAL)
 ``F_CLOCK_COMP c
    (F_SUFFIX_IMP
     ((S_REPEAT(S_BOOL B_TRUE) ;;
       S_BOOL(B_NOT(B_PROP ak1)) ;; 
       S_BOOL(B_PROP ak1) ;;
       S_BOOL B_TRUE),
      F_BEFORE
       (F_AND(F_NOT(F_BOOL(B_PROP ak2)), 
              F_NEXT(F_BOOL(B_PROP ak2))),
        F_AND(F_NOT(F_BOOL(B_PROP ak1)), 
              F_NEXT(F_BOOL(B_PROP ak1))))))``;

(*  
** {[*]; !StoB_REQ & BtoS_ACK; StoB_REQ}(F)@clk1  
*)
time
 EVAL
 ``UF_SEM
    (FINITE SimRun)
    (F_CLOCK_COMP
      (B_PROP clk1)
      (F_SUFFIX_IMP
        (S_CAT(S_REPEAT S_TRUE, 
               S_CAT(S_BOOL(B_AND(B_NOT(B_PROP StoB_REQ), B_PROP BtoS_ACK)),
                     S_BOOL(B_PROP StoB_REQ))),
         F_BOOL B_FALSE)))``;

(*  
** {[*]; !StoB_REQ & BtoS_ACK; StoB_REQ}(F)@(clk1 or clk2 or clk3)
*)
time
 EVAL
 ``UF_SEM
    (FINITE SimRun)
    (F_CLOCK_COMP
      (BOOL_OR(B_PROP clk1, BOOL_OR(B_PROP clk2, B_PROP clk3)))
      (F_SUFFIX_IMP
        (S_CAT(S_REPEAT S_TRUE, 
               S_CAT(S_BOOL(B_AND(B_NOT(B_PROP StoB_REQ), B_PROP BtoS_ACK)),
                     S_BOOL(B_PROP StoB_REQ))),
         F_BOOL B_FALSE)))``;







